proposition: Lemma sep__sep_mon : forall (i : nat) (Hi : i <= n) (Hi' : S i <= n), sep__sep_fun i Hi[<]sep__sep_fun (S i) Hi'.
proof: Proof. intros. unfold sep__sep_fun in |- *. elim (le_lt_dec (S i) 0); intro; simpl in |- *. exfalso; apply (Nat.nle_succ_0 _ a0). elim (le_lt_dec i 0); intro; simpl in |- *. elim (le_lt_eq_dec _ _ Hi'); intro; simpl in |- *. apply less_leEq_trans with (P (S i) Hi'). apply leEq_less_trans with (P i Hi). elim (Partition_in_compact _ _ _ _ P i Hi); intros; auto. apply HP. apply sep__sep_leEq. assumption. elim (le_lt_eq_dec _ _ Hi); intro; simpl in |- *. elim (le_lt_eq_dec _ _ Hi'); intro; simpl in |- *. apply sep__sep_mon_i; assumption. eapply less_wdr. 2: apply finish with (p := P) (H := le_n n). eapply less_wdr. apply sep__sep_less with (Hi' := Hi'). generalize Hi'; rewrite b2. intro; apply prf1; auto. exfalso; rewrite b2 in Hi'; apply (Nat.nle_succ_diag_l _ Hi'). Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions