proposition: Lemma sep__sep_lemma : Separated sep__sep_part R.
proof: Proof. repeat split; unfold _Separated in |- *; intros. apply sep__sep_mon. apply HR. unfold sep__sep_part in |- *; simpl in |- *. unfold sep__sep_fun in |- *; simpl in |- *. elim (le_lt_dec i 0); intro; simpl in |- *. exfalso; apply Nat.lt_irrefl with 0; apply Nat.lt_le_trans with i; auto. elim (le_lt_eq_dec _ _ Hi); intro; simpl in |- *. apply sep__sep_ap. exfalso; rewrite b1 in H1; apply (Nat.lt_irrefl _ H1). Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions