proposition: Lemma gcd_ind : forall P : nat -> nat -> Prop, (forall x : nat, P 0 x) -> (forall x : nat, P x 0) -> (forall a b : nat, P a b -> P a (b + a)) -> (forall a b : nat, P a b -> P (a + b) b) -> forall a b : nat, P a b.
proof: Proof. intros P H H0 H1 H2 a; pattern a in |- *; apply lt_wf_ind. intros a' H' b; pattern b in |- *; apply lt_wf_ind. intros b' H'0. case (zerop a'); intros lta'; [ rewrite lta'; auto | idtac ]. case (zerop b'); intros ltb'; [ rewrite ltb'; auto | idtac ]. case (lt_eq_lt_dec a' b'); intros Ca'b'; [ case Ca'b'; clear Ca'b'; intros Ca'b' | idtac ]. replace b' with (b' - a' + a'); auto with arith; rewrite Nat.add_comm; auto with arith. replace b' with (0 + b'); [ rewrite Ca'b' | idtac ]; auto with arith. replace a' with (a' - b' + b'); auto with arith; rewrite Nat.add_comm; auto with arith. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)