proposition: Lemma continuous_imp_monotonic : forall f, reflexive R -> continuous f -> monotonic f.
proof: Proof. intros f Hr Hc x y Hxy. assert (Hl : lub R' (f y) (fun n => f (match n with 0 => x | _ => y end))). apply (Hc (fun n => match n with 0 => x | _ => y end)). unfold chain; destruct n; auto. split. unfold upper_bound; destruct n; auto. intros b H; exact (H 1). destruct Hl as [Hu Hl']; exact (Hu 0). Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith