proposition: Lemma inject_Q_mult : forall q r : Q, inject_Q (q * r) == inject_Q q * inject_Q r.
proof: Proof. split. - intros [n maj]; cbn in maj. unfold CReal_mult_seq in maj; cbn in maj. pose proof Qpower_0_lt 2 n; lra. - intros [n maj]; cbn in maj. unfold CReal_mult_seq in maj; cbn in maj. pose proof Qpower_0_lt 2 n; lra. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra