proposition: Lemma sup_tail_decrease : forall m n : nat, m <= n -> sup_tail n[<=]sup_tail m.
proof: Proof. intros. rewrite -> leEq_def; intro. case (Psup_unfolded2 (tail_seq g n) (sup_tail m)). assumption. intro xj. intros H2 H3. red in H2. case H2. intro j. intros. apply (less_irreflexive_unfolded _ xj). apply leEq_less_trans with (y := sup_tail m). apply leEq_wdl with (x := CS_seq OF (tail_seq g n) j). simpl in |- *. apply sup_tail_leEq. apply Nat.le_trans with (m := n). assumption. apply Nat.le_add_r. apply eq_symmetric_unfolded. assumption. assumption. Qed.
imports: CoRN.reals.Bridges_LUB