proposition: Lemma RSR_H' : forall i j : nat, 0 < i -> 0 < j -> i < n -> j < m -> forall (Hi : i <= n) (Hj : j <= m), P i Hi[#]R j Hj.
proof: Proof. elim HPR; do 2 intro. elim b0; do 2 intro; assumption. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)