proposition: Lemma ratSubtract_half : forall x, ratSubtract x (x * (1/2)) == x * (1/2).
proof: Proof. intuition. unfold ratSubtract. rattac. arithNormalize. inversion H; clear H; subst. rewrite <- (Nat.mul_assoc (n * x * 2)). rewrite (Nat.mul_comm (n * x)). repeat rewrite Nat.mul_assoc. simpl. rewrite (Nat.add_0_r). repeat rewrite Nat.mul_add_distr_r. remember (n * x * x * 2)%nat as a. lia. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms