proposition: Lemma Rsqr_eq_0_reg : forall a, a * a = 0 -> a = 0.
proof: Proof. intros a Haa. destruct (total_order_T a 0) as [[|]|]; subst; trivial; (cut (0 < a * a); [intro; apply False_ind; apply (Rlt_not_eq _ _ H); auto|]); [replace (a * a) with (- a * - a) by ring|]; apply Rmult_lt_0_compat; lra. Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions