proposition: Lemma RSR_f'_mon : forall (i i' : nat) Hi Hi', i < i' -> f' i Hi[<]f' i' Hi'.
proof: Proof. intros. apply local_mon_imp_mon_lt with (n := pred n). intros; unfold f' in |- *; apply RSR_HP. assumption. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)