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