proposition: Lemma length_tail_cut_cons : forall (x y : A) l, length (tail (cut x (y::l))) <= length l.
proof: Proof. intros. simpl. destruct (eq_dec x y); simpl. trivial. apply Nat.le_trans with (length (cut x l)). apply length_tail. apply length_cut. Qed.
imports: Coq(PeanoNat) CoLoR(ListUtil ListNodup LogicUtil RelMidex)