proposition: Lemma N_pos_div_eucl_rest : forall i b q r, N.pos_div_eucl i (N.pos b) = (q, r) -> (0 < r)%N -> (0 < q)%N -> (b * N2pos q + N2pos r)%positive = i.
proof: Proof. intros i b q r H H0 H1. generalize (N.pos_div_eucl_spec i (N.pos b)). rewrite H. destruct r ;[discriminate | ]. destruct q ; [discriminate | ]. injection 1. cbn. intro H3;subst i. now rewrite Pos.mul_comm. Qed.
imports: Coq(Arith NArith Lia Recdef) additions(Pow Compatibility Wf_transparent)