proposition: Lemma a_b' : forall i j : nat, a i [<] b j.
proof: Proof. intros. elim (le_lt_dec i j); intro. apply leEq_less_trans with (a j). apply a_mon'. auto. auto. apply less_leEq_trans with (b i). auto. apply b_mon'. auto with arith. Qed.
imports: CoRN.reals.CPoly_Contin