proposition: Lemma inverse_image_increasing: forall {X Y:Type} (f:X->Y) (T1 T2:Ensemble Y), Included T1 T2 -> Included (inverse_image f T1) (inverse_image f T2).
proof: Proof. intros. red; intros. destruct H0. constructor. auto. Qed.
imports: FunctionProperties Ensembles EnsemblesImplicit EnsemblesSpec