proposition: Lemma Zpos_div_eucl_aux1_correct : forall a b, Zpos_div_eucl_aux1 a b = Z.pos_div_eucl a (Zpos b).
proof: Proof. intros a b. revert a. induction b ; intros a. - easy. - change (Z.pos_div_eucl a (Zpos b~0)) with (Z.div_eucl (Zpos a) (Zpos b~0)). rewrite Zdiv_eucl_unique. change (Zpos b~0) with (2 * Zpos b)%Z. rewrite Z.rem_mul_r by easy. rewrite <- Zdiv_Zdiv by easy. destruct a as [a|a|]. + change (Zpos_div_eucl_aux1 a~1 b~0) with (let (q, r) := Zpos_div_eucl_aux1 a b in (q, 2 * r + 1)%Z). rewrite IHb. clear IHb. change (Z.pos_div_eucl a (Zpos b)) with (Z.div_eucl (Zpos a) (Zpos b)). rewrite Zdiv_eucl_unique. change (Zpos a~1) with (1 + 2 * Zpos a)%Z. rewrite (Zmult_comm 2 (Zpos a)). rewrite Z_div_plus_full by easy. apply f_equal. rewrite Z_mod_plus_full. apply Zplus_comm. + change (Zpos_div_eucl_aux1 a~0 b~0) with (let (q, r) := Zpos_div_eucl_aux1 a b in (q, 2 * r)%Z). rewrite IHb. clear IHb. change (Z.pos_div_eucl a (Zpos b)) with (Z.div_eucl (Zpos a) (Zpos b)). rewrite Zdiv_eucl_unique. change (Zpos a~0) with (2 * Zpos a)%Z. rewrite (Zmult_comm 2 (Zpos a)). rewrite Z_div_mult_full by easy. apply f_equal. now rewrite Z_mod_mult. + easy. - change (Z.pos_div_eucl a 1) with (Z.div_eucl (Zpos a) 1). rewrite Zdiv_eucl_unique. now rewrite Zdiv_1_r, Zmod_1_r. Qed.
imports: Coq(ZArith Lia Zquot)