proposition: Lemma cc_csg_associative : associative cc_plus_op.
proof: Proof. unfold associative in |- *. intros. elim x. elim y. elim z. intros. simpl in |- *. unfold cc_eq in |- *. simpl in |- *. split; algebra. Qed.
imports: CoRN.reals.NRootIR