proposition: Theorem gcd_inv_Or_aux : forall a b c : nat, gcd_spec a b c -> b = 0 -> a = c.
proof: Proof. intros a b c H'; elim H'; auto. intros a0 b0 c0 H'0 H'1 H'2 H'3. apply H'2; auto. rewrite H'3; auto. intros a0 b0 c0 H'0 H'1 H'2 H'3. replace a0 with (a0 - b0); auto. rewrite H'3; auto with arith. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)