proposition: Lemma sep__part_fun_wd : forall (i j : nat) Hi Hj, i = j -> sep__part_fun i Hi = sep__part_fun j Hj.
proof: Proof. intros. unfold sep__part_fun in |- *. elim (le_lt_eq_dec _ _ Hi); elim (le_lt_eq_dec _ _ Hj); intros; simpl in |- *. rewrite H; auto. rewrite H in a0; rewrite b0 in a0; elim (Nat.lt_irrefl _ a0). rewrite <- H in a0; rewrite b0 in a0; elim (Nat.lt_irrefl _ a0). auto. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)