proposition: Lemma ratSubtract_ratAdd_distr : forall r1 r2 r3, ratSubtract r1 (r2 + r3) == ratSubtract (ratSubtract r1 r2) r3.
proof: Proof. intuition. unfold ratSubtract, ratAdd. rattac. arithNormalize. rewrite Nat.sub_add_distr. f_equal. f_equal. do 5 arithSimplify. do 5 arithSimplify. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms