proposition: Lemma CRplus_eq_compat_l : forall {R : ConstructiveReals} (a b c : CRcarrier R), b == c -> a + b == a + c.
proof: Proof. intros. rewrite H. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions