proposition: Lemma Nquotient_le_compat : forall a b c q p, Nquotient a b q -> Nquotient a c p -> 1 <= b <= c -> q <= p.
proof: Proof. intros. assert (1<=a). apply Ndiv_non_0 with b. apply Nquotient_div with q. exact H. destruct H1. exact H1. assert (exists a',a=S a'). destruct a. apply Nat.nle_succ_0 in H2. contradiction. exists a. reflexivity. destruct H3. destruct H. destruct H0. destruct H1. rewrite H in H4. rewrite H0 in H4. rewrite H3 in H4. apply Nat.mul_le_mono_pos_l with (S x). apply Nat.lt_0_succ. assert (S x*q=q*S x). ring. assert (S x*q0=q0*S x). ring. rewrite H5. rewrite H6. exact H4. Qed.
imports: Coq(Arith Euclid Compare Lia)