proposition: Lemma pos_AntiMesh : forall n (P : Partition Hab n), 0 < n -> _Separated P -> [0] [<] AntiMesh P.
proof: Proof. intro; case n; clear n. intros P H H0; exfalso; apply (Nat.lt_irrefl _ H). intros n P H H0. unfold AntiMesh in |- *. apply less_minlist. simpl in |- *; auto with arith. intros y H1. elim (Part_Mesh_List_lemma _ _ _ _ _ _ H1); intros i Hi. elim Hi; clear Hi; intros Hi Hi'. elim Hi'; clear Hi'; intros Hi' H'. eapply less_wdr. 2: apply eq_symmetric_unfolded; apply H'. apply shift_less_minus; astepl (P i Hi). apply H0. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)