proposition: Lemma compose_pres_mult : fun_pres_bin_fun R1 R3 compose (cr_mult (c:=R1)) (cr_mult (c:=R3)).
proof: Proof. red in |- *. unfold compose in |- *. case f. intro f_. intros f_1 f_2 f_3 f_4. cut (fun_wd g). case g. intro g_. intros g_1 g_2 g_3 g_4. intros. simpl in H. simpl in |- *. astepl (g_ (f_ x[*]f_ y)). apply g_4. red in |- *. intros. apply map_wd_unfolded. assumption. Qed.
imports: CoRN.reals.CReals