proposition: Lemma pos_div_eucl_quotient_pos : forall a b q r, N.pos_div_eucl a b = (q, r) -> (b <= N.pos a)%N -> b <> 0%N -> (q <> 0%N).
proof: Proof. intros a b q r H H1; generalize (N.pos_div_eucl_spec a b); rewrite H. intros H0 H2 H3. rewrite H3 in H0 ; simpl in H0. generalize (N.pos_div_eucl_remainder a b H2); rewrite H; simpl; intro; subst r. destruct (N.lt_irrefl b);auto. apply N.le_lt_trans with (N.pos a);auto. Qed.
imports: Coq(Arith NArith Lia Recdef) additions(Pow Compatibility Wf_transparent)