proposition: Theorem is_gcd_inv : forall a b c : nat, is_gcd a (a + b) c -> is_gcd a b c.
proof: Proof. intros a b c (H1, (H2, H3)); split; auto; split; auto. apply divides_plus2 with (2 := H2); auto. intros d H4 H5; apply H3; auto. apply divides_plus1; auto. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)