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