proposition: Lemma RSR_h_mon : forall (i i' : nat) Hi Hi', i < i' -> h i Hi[<]h i' Hi'.
proof: Proof. unfold h in |- *; apply om_fun_2; auto. exact RSR_f'_nlnf. exact RSR_g'_nlnf. exact RSR_f'_mon. exact RSR_g'_mon. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)