proposition: Lemma Zpos_div_eucl_aux_correct : forall a b, Zpos_div_eucl_aux a b = Z.pos_div_eucl a (Zpos b).
proof: Proof. intros a b. unfold Zpos_div_eucl_aux. change (Z.pos_div_eucl a (Zpos b)) with (Z.div_eucl (Zpos a) (Zpos b)). rewrite Zdiv_eucl_unique. case Pos.compare_spec ; intros H. now rewrite H, Z_div_same, Z_mod_same. now rewrite Zdiv_small, Zmod_small by (split ; easy). rewrite Zpos_div_eucl_aux1_correct. change (Z.pos_div_eucl a (Zpos b)) with (Z.div_eucl (Zpos a) (Zpos b)). apply Zdiv_eucl_unique. Qed.
imports: Coq(ZArith Lia Zquot)