coq_practice_36.v

Require Import ZArith.

Section Principal_Ideal.
  Variable a : Z.

  Definition pi : Set := { x : Z | ( a | x )%Z }.

  Program Definition plus(a b : pi) : pi := (a + b)%Z.
  Next Obligation.
    unfold proj1_sig.
    unfold Z.divide.
    destruct a0.
    destruct b.
    destruct d.
    destruct d0.
    exists (x1+x2)%Z.
    rewrite H.
    rewrite H0.
    ring.
  Qed.

  Program Definition mult(a : Z) (b : pi) : pi := (a * b)%Z.
  Next Obligation.
    unfold proj1_sig.
    unfold Z.divide.
    destruct b.
    destruct d.
    rewrite H.
    exists (a0 * x0)%Z.
    ring.
  Qed.
End Principal_Ideal.