proposition: Lemma RSR_g'_mon : forall (j j' : nat) Hj Hj', j < j' -> g' j Hj[<]g' j' Hj'.
proof: Proof. intros. apply local_mon_imp_mon_lt with (n := pred m). intros; unfold g' in |- *; apply RSR_HR. assumption. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)