proposition: Lemma pos_div_eucl_quotient_lt : forall a b q r, N.pos_div_eucl a b = (q, r) -> (1 < b)%N -> (q < N.pos a)%N.
proof: Proof. intros a b q r H H1; generalize (N.pos_div_eucl_spec a b); rewrite H. destruct q. - reflexivity. - intro H2; rewrite H2; apply N.lt_le_trans with (N.pos p * b)%N. + replace (N.pos p) with ((N.pos p) * 1)%N at 1 by (now rewrite N.mul_1_r). apply N.mul_lt_mono_pos_l; auto with chains. + apply N.le_add_r. Qed.
imports: Coq(Arith NArith Lia Recdef) additions(Pow Compatibility Wf_transparent)