proposition: Lemma gcd_log2_Zle : forall c1 c2 a b, log2 c1 <= log2 c2 -> gcd_log2 a b c1 <> None -> gcd_log2 a b c2 = gcd_log2 a b c1.
proof: Proof. Proof with zsimpl;trivial;try lia. induction c1;destruct c2;simpl;intros; (destruct (a mod b) as [|r];[idtac | destruct (b mod r)]) ... apply IHc1;trivial. generalize H;zsimpl;intros;lia. apply IHc1;trivial. generalize H;zsimpl;intros;lia. apply IHc1;trivial. generalize H;zsimpl;intros;lia. apply IHc1;trivial. generalize H;zsimpl;intros;lia. elim H0;trivial. elim H0;trivial. Qed.
imports: ZArith Lia ZCmisc