proposition: Lemma RS'_pos_m : 0 < m.
proof: Proof. unfold m in |- *. elim (RS'_delta2_delta4 RS'_m1); intro; simpl in |- *. auto with arith. elim (ProjT2 sep__part_app_n); fold RS'_m1 in |- *; intros. cut (0 <> RS'_m1); intro. auto with arith. exfalso. apply less_irreflexive_unfolded with (x := delta [/]TwoNZ). apply less_transitive_unfolded with (b[-]a). assumption. eapply less_wdl. apply b0. apply cg_minus_wd. eapply eq_transitive_unfolded. 2: apply finish with (p := P) (H := le_n n). apply prf1. auto. eapply eq_transitive_unfolded. 2: apply start with (p := P) (H := Nat.le_0_l n). apply prf1. rewrite <- H1. simpl in |- *; auto. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)