proposition: Lemma ratSubtract_0_r : forall r, ratSubtract r 0 == r.
proof: Proof. unfold ratSubtract in *. rattac. arithNormalize. inversion H; clear H; subst. simpl. rewrite Nat.sub_0_r. do 2 arithSimplify. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms