proposition: Lemma compose_pres_less : fun_pres_relation R1 R3 compose (cof_less (c:=R1)) (cof_less (c:=R3)).
proof: Proof. red in |- *. unfold compose in |- *. case f. intro f_. intros f_1 f_2 f_3 f_4. case g. intro g_. intros g_1 g_2 g_3 g_4. intros. simpl in |- *. apply g_2. apply f_2. assumption. Qed.
imports: CoRN.reals.CReals