proposition: Lemma continuous_reverse : forall (f:A->B)(c :nat->A), antisymmetric R' -> chain R c -> continuous f -> forall (l:A), lub R l c -> forall (l':B), lub R' l' (fun n => f (c n)) -> l' = f l.
proof: Proof. intros f c Ha Hch Hct l Hlub l' Hlub'. assert (Hlub2 : lub R' (f l)(fun n => f (c n))). exact (Hct c Hch l Hlub). apply (unique_lub B R' (fun n => f (c n))); assumption. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith