proposition: Theorem Qpositive_le_to_Qpositive_le' : forall w w' : Qpositive, Qpositive_le w w' -> Qpositive_le' w w'.
proof: Proof. intros w w'; generalize w; elim w'; clear w w'. intros w'1 Hrec w; case w. unfold Qpositive_le in |- *; simpl in |- *. intros w1 H; generalize (Hrec w1 H). unfold Qpositive_le' in |- *. simpl in |- *. case (Qpositive_i w1); case (Qpositive_i w'1). intros p' q' p q Hle; repeat rewrite Nat.mul_add_distr_r. rewrite (Nat.mul_comm q'). apply Nat.add_le_mono_r. auto. intros w1; unfold Qpositive_le in |- *. simpl in |- *. unfold Qpositive_le' in |- *; simpl in |- *; intros H; case (Qpositive_i w1); case (Qpositive_i w'1); intros p' q' p q. rewrite Nat.mul_add_distr_r. repeat rewrite <- (Nat.mul_comm (p + q)). repeat rewrite Nat.mul_add_distr_r. rewrite (Nat.add_comm (p * p' + q * p')). repeat rewrite <- Nat.add_assoc. auto with arith. unfold Qpositive_le, Qpositive_le' in |- *. simpl in |- *. case (Qpositive_i w'1). intros; lia. intros w'1 Hrec w; case w; clear w; unfold Qpositive_le in |- *; simpl in |- *. intros q H; discriminate H. intros w1 H; generalize (Hrec w1 H); unfold Qpositive_le' in |- *. simpl in |- *; case (Qpositive_i w1); case (Qpositive_i w'1); intros p' q' p q. repeat rewrite (Nat.mul_comm p); repeat rewrite (Nat.mul_comm p'); repeat rewrite Nat.mul_add_distr_r. intros H1. rewrite (Nat.mul_comm p'). apply Nat.add_le_mono_l. auto. intros H; discriminate H. unfold Qpositive_le, Qpositive_le' in |- *. intros w; case w. 3: simpl in |- *; auto. intros w1; simpl in |- *. intros Heq; discriminate Heq. intros w'; simpl in |- *. case (Qpositive_i w'). intros; lia. Qed.