proposition: Lemma cc_inv_strext : un_op_strext cc_csetoid cc_inv.
proof: Proof. unfold un_op_strext in |- *. unfold fun_strext in |- *. intros x y. elim x. elim y. simpl in |- *. unfold cc_ap in |- *. simpl in |- *. do 4 intro. intro H. elim H; clear H; intros. left. apply un_op_strext_unfolded with (cg_inv (c:=IR)). auto. right. apply un_op_strext_unfolded with (cg_inv (c:=IR)). auto. Qed.
imports: CoRN.reals.NRootIR