proposition: Lemma mindropeq_nthP x0 s t p : x0 \notin s -> x0 \notin t -> reflect (nth x0 s p != nth x0 t p /\ (forall i, i > p -> nth x0 s i = nth x0 t i)) (mindropeq s t == p.+1).
proof: Proof. rewrite /mindropeq => x0notins x0notint. apply (iffP eqP); case: ex_minnP => m eqdrop mmin. - move=> eqmp1; split. + move/(_ p)/contra: mmin; rewrite eqmp1 -leqNgt => /(_ (leqnn _)) Hneq. rewrite {}eqmp1 -add1n -!drop_drop in eqdrop. apply/contra: Hneq => /eqP; rewrite -{1 2}(addn0 p) -!nth_drop => Heq. have {x0notins} : x0 \notin (drop p s). by apply/contra/mem_drop: x0notins. have {x0notint} : x0 \notin (drop p t). by apply/contra/mem_drop: x0notint. case: (drop p s) (drop p t) Heq eqdrop => [|s0 s'] [|t0 t'] //= <-; try by rewrite inE eqxx /=. by rewrite !drop0 => /eqP ->. + rewrite -eqmp1 => i lemi. by rewrite -(subnKC lemi) -!nth_drop (eqP eqdrop). - move=> [Hneq Heq]. apply anti_leq; apply/andP; split. + apply: mmin; apply/eqP/(eq_from_nth_notin (x0 := x0)); first last. by move=> i; rewrite !nth_drop addSn; apply: Heq; rewrite ltnS leq_addr. * by apply/contra: x0notint => /mem_drop. * by apply/contra: x0notins => /mem_drop. + apply/contraR: Hneq; rewrite -leqNgt => lemp. by rewrite -(subnKC lemp) -!nth_drop (eqP eqdrop). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition