proposition: Lemma f_bottom {f : A -> B} : morph f -> L.eq (f bottom) bottom.
proof: Proof. intros MF. unfold bottom. rewrite (f_sup MF). apply sup_proper. unfold pointwise_relation. intros. contradiction. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat