proposition: Lemma RSR_h_mon' : forall (i i' : nat) Hi Hi', i <= i' -> h i Hi[<=]h i' Hi'.
proof: Proof. intros; apply mon_imp_mon'_lt with (n := pred m + pred n). apply RSR_h_nlnf. apply RSR_h_mon. assumption. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)