proposition: Lemma ratSubtract_leRat_r : forall r1 r2 r3, r1 <= r2 -> ratSubtract r3 r2 <= ratSubtract r3 r1.
proof: Proof. rattac. unfold ratSubtract in *. rattac. unfold posnatMult in *. inversion H4; clear H4; subst. inversion H3; clear H3; subst. arithNormalize. assert (n * x3 * x3 * x1 <= n0 * x3 * x3 * x2)%nat. rewrite <- Nat.mul_comm. rewrite <- (Nat.mul_comm x2). repeat rewrite Nat.mul_assoc. eapply Nat.mul_le_mono; trivial. eapply Nat.mul_le_mono; trivial. rewrite Nat.mul_comm. rewrite l. rewrite Nat.mul_comm. trivial. assert (n3 * x1 * x3 * x2 = n3 * x2 * x3 * x1)%nat. do 3 arithSimplify. lia. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms