proposition: Lemma ratSubtract_ratAdd_assoc_le : forall r1 r2 r3, ratSubtract (r1 + r2) r3 <= r1 + (ratSubtract r2 r3).
proof: Proof. unfold ratSubtract, ratAdd. rattac. arithNormalize. generalize (n1 * x0 * x1 * x * x0 * x1)%nat; intuition idtac. assert (n3 * x * x1 * x * x0 * x1 = n3 * x1 * x * x * x0 * x1)%nat. do 5 arithSimplify. rewrite H. generalize (n3 * x1 * x * x * x0 * x1)%nat; intuition idtac. assert (n0 * x * x0 * x * x0 * x1 = n0 * x0 * x * x * x0 * x1)%nat. do 5 arithSimplify. rewrite H0. generalize ( n0 * x0 * x * x * x0 * x1)%nat; intros ?; lia. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms