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