proposition: Lemma Qpositive_le_noneq_explicit: forall qp qp', Qpositive_le qp qp' -> ~ qp=qp' -> let (p, q) := Qpositive_i qp in let (p', q') := Qpositive_i qp' in (p * q' < p' * q)%nat.
proof: Proof. intros qp qp' H_le H_neq; generalize (Qpositive_le_to_Qpositive_le' qp qp' H_le); unfold Qpositive_le'; destruct (interp_non_zero qp) as [p [q H]]; destruct (interp_non_zero qp') as [p' [q' H']]; rewrite H; rewrite H'; intros H_le_unfold; destruct (le_lt_eq_dec _ _ H_le_unfold) as [H1|H1]; trivial; apply False_ind; apply H_neq; rewrite <- (construct_correct qp (S p) (S q) (S p+S q)%nat H); auto with arith; rewrite <- (construct_correct qp' (S p') (S q') (S p'+S q')%nat H'); auto with arith; apply construct_correct4'; auto with arith. Qed.