proposition: Lemma inv_is_mono : is_iso E F f -> is_mono F invf.
proof: Proof. intros. red in |- *. intros x y dans_x dans_y egal_inv. replace x with (f (inv E F f x)). replace y with (f (inv E F f y)). apply (f_equal (A:=Elt) (B:=Elt)); assumption. auto. auto. Qed.
imports: Ensf Words more_words need