proposition: Lemma ratOneHalf_add: 1 / 2 + 1 / 2 == 1.
proof: Proof. unfold ratAdd. simpl. unfold posnatMult. simpl. apply (@num_dem_same_rat1 4 _). simpl. trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms