proposition: Lemma N_pos_div_eucl_divides : forall i b q, N.pos_div_eucl i (N.pos b) = (q, 0%N) -> (b * N2pos q)%positive = i.
proof: Proof. intros i b q H; generalize (N.pos_div_eucl_spec i (N.pos b)). rewrite H, N.add_0_r. intro H3; destruct q ; [discriminate | ]. rewrite Pos.mul_comm; injection H3; symmetry; assumption. Qed.
imports: Coq(Arith NArith Lia Recdef) additions(Pow Compatibility Wf_transparent)