proposition: Lemma _Separated_imp_length_zero : forall n (P : Partition Hab n), _Separated P -> a [=] b -> 0 = n.
proof: Proof. intros n P H H0. cut (~ 0 <> n); [ auto with zarith | intro ]. cut (0 < n); [ intro | apply Nat.neq_0_lt_0; auto ]. cut (a [#] b). exact (eq_imp_not_ap _ _ _ H0). astepl (P _ (Nat.le_0_l _)). astepr (P _ (le_n _)). apply less_imp_ap. apply local_mon_imp_mon_le with (f := fun (i : nat) (H : i <= n) => P i H). exact H. assumption. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)