proposition: Lemma compose_strext : fun_strext compose.
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. rename X into H. simpl in H. apply f_1. apply g_1. assumption. Qed.
imports: CoRN.reals.CReals