proposition: Lemma Cplus_assoc (x y z : C) : x + (y + z) = (x + y) + z.
proof: Proof. apply injective_projections ; simpl ; apply sym_eq, Rplus_assoc. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy