proposition: Lemma Rplus_half_diag : forall r, r / 2 + r / 2 = r.
proof: Proof. intros r; rewrite <-Rdiv_plus_distr, Rplus_diag, Rmult_div_r; [easy |]. now apply not_eq_sym, Rlt_not_eq, Rlt_0_2. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField