proposition: Lemma CReal_mult_comm : forall x y : CReal, x * y == y * x.
proof: Proof. assert (forall x y : CReal, x * y <= y * x) as H. { intros x y [n nmaj]. apply (Qlt_not_le _ _ nmaj). clear nmaj. unfold CReal_mult, CReal_mult_seq; do 2 rewrite CReal_red_seq. ring_simplify. pose proof Qpower_0_lt 2 n ltac:(lra); lra. } split; apply H. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra