proposition: Lemma b_mon' : forall i j : nat, i <= j -> b j [<=] b i.
proof: Proof. intros. set (b' := fun i : nat => [--] (b i)) in *. astepl ( [--][--] (b j)). astepr ( [--][--] (b i)). fold (b' i) (b' j) in |- *. apply inv_resp_leEq. apply local_mon'_imp_mon'. unfold b' in |- *; intro; apply inv_resp_leEq; auto. auto. Qed.
imports: CoRN.reals.CPoly_Contin