proposition: Lemma RS'_m_m1 : {m = RS'_m1} + {m = S RS'_m1}.
proof: Proof. unfold m in |- *. elim (RS'_delta2_delta4 RS'_m1); intro; simpl in |- *. right; auto. left; auto. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)