proposition: Lemma sep__sep_fun_wd : forall i j : nat, i = j -> forall (Hi : i <= n) (Hj : j <= n), sep__sep_fun i Hi[=]sep__sep_fun j Hj.
proof: Proof. intros. unfold sep__sep_fun in |- *. elim (le_lt_dec i 0); elim (le_lt_dec j 0); intros; simpl in |- *. algebra. exfalso; apply (Nat.lt_irrefl 0); apply Nat.lt_le_trans with j; auto; rewrite <- H; auto. exfalso; apply (Nat.lt_irrefl 0); apply Nat.lt_le_trans with j; auto; rewrite <- H; auto. elim (le_lt_eq_dec _ _ Hi); elim (le_lt_eq_dec _ _ Hj); intros; simpl in |- *. apply sep__sep_fun_i_wd; auto. exfalso; rewrite H in a0; rewrite b2 in a0; apply (Nat.lt_irrefl _ a0). exfalso; rewrite <- H in a0; rewrite b2 in a0; apply (Nat.lt_irrefl _ a0). algebra. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions