proposition: Lemma I_square : II[*]II [=] [--][1].
proof: Proof. simpl in |- *. unfold cc_mult in |- *. simpl in |- *. unfold cc_inv in |- *. simpl in |- *. split. simpl in |- *. rational. simpl in |- *. rational. Qed.
imports: CoRN.reals.NRootIR