proposition: Lemma Zis_gcd_mod : forall a b d, 0 < b -> Zis_gcd b (a mod b) d -> Zis_gcd a b d.
proof: Proof. intros a b d H H1; apply Zis_gcd_for_euclid with (a/b). pattern a at 1;rewrite (Z_div_mod_eq_full a b). ring_simplify (b * (a / b) + a mod b - a / b * b);trivial. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub