proposition: Lemma cc_cg_proof : is_CGroup cc_cmonoid cc_inv_op.
proof: Proof. unfold is_CGroup in |- *. intros. elim x. intros. split. simpl in |- *. unfold cc_eq in |- *. simpl in |- *. split; algebra. simpl in |- *. unfold cc_eq in |- *. simpl in |- *. split; algebra. Qed.
imports: CoRN.reals.NRootIR