proposition: Lemma cc_mult_strext : bin_op_strext cc_csetoid cc_mult.
proof: Proof. unfold bin_op_strext in |- *. unfold bin_fun_strext in |- *. intros x1 x2 y1 y2. elim x1. elim x2. elim y1. elim y2. simpl in |- *. unfold cc_ap in |- *. simpl in |- *. do 8 intro. intro H. elim H; clear H; intros H. elim (bin_op_strext_unfolded _ (cg_minus_is_csetoid_bin_op _) _ _ _ _ H); intros H0. elim (bin_op_strext_unfolded _ _ _ _ _ _ H0); intros H1. left. left. auto. right. left. auto. cut (Im3[*]Im1 [#] Im2[*]Im0). intro H1. elim (bin_op_strext_unfolded _ _ _ _ _ _ H1); intros H2. left. right. auto. right. right. auto. auto. elim (bin_op_strext_unfolded _ _ _ _ _ _ H); intros H0. elim (bin_op_strext_unfolded _ _ _ _ _ _ H0); intros H1. left. left. auto. right. right. auto. elim (bin_op_strext_unfolded _ _ _ _ _ _ H0); intros. left. right. auto. right. left. auto. Qed.
imports: CoRN.reals.NRootIR