proposition: Lemma sep__part_fun_0 : forall H : 0 <= m, sep__part_fun 0 H = 0.
proof: Proof. intros. unfold sep__part_fun in |- *. elim (le_lt_eq_dec _ _ H); intro; simpl in |- *. reflexivity. exfalso. generalize b0. apply Nat.neq_sym. apply Nat.neq_0_lt_0; apply RS'_pos_m. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)