proposition: Lemma CC_conj_strext : forall c c' : CC, CC_conj c [#] CC_conj c' -> c [#] c'.
proof: Proof. intros c c'. elim c. intros x y. elim c'. intros x' y'. simpl in |- *. unfold cc_ap in |- *. simpl in |- *. intros H. elim H; clear H; intros. left. auto. right. apply un_op_strext_unfolded with (cg_inv (c:=IR)). auto. Qed.
imports: CoRN.reals.NRootIR