proposition: Lemma gcd_mod0 : forall a b, (a mod b)%P = N0 -> gcd a b = b.
proof: Proof. intros a b H;unfold gcd. pattern (gcd_log2 a b (xO b)) at 1; rewrite (gcd_log2_mod0 _ _ (xO b) H);trivial. Qed.
imports: ZArith Lia ZCmisc Zwf