proposition: Lemma RSR_h_f' : forall (i : nat) Hi, {j : nat | {Hj : _ < _ | f' i Hi[=]h j Hj}}.
proof: Proof. unfold h in |- *; apply om_fun_3a; auto. exact RSR_f'_nlnf. exact RSR_g'_nlnf. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)