proposition: Theorem ratHalf_add : forall r, ratHalf r + ratHalf r == r.
proof: Proof. intuition. unfold ratHalf. eapply eqRat_trans. apply eqRat_symm. apply ratMult_distrib. eapply eqRat_trans. apply ratMult_eqRat_compat. apply eqRat_refl. apply ratOneHalf_add. rewrite ratMult_1_r. intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms