proposition: Lemma Zgcd_minus: forall a b d:Z, Zis_gcd a (b - a) d -> Zis_gcd a b d.
proof: Proof. intros a b d H; case H; constructor; intuition (auto with zarith). replace b with (b-a+a)%Z. auto with zarith. lia. Qed.
imports: ZArith Znumtheory hoarelogic Zwf Wellfounded Lia