proposition: Lemma length_cut : forall (x : A) l, length (cut x l) <= length l.
proof: Proof. induction l; simpl. apply Nat.le_0_l. destruct (eq_dec x a). apply Nat.le_refl. apply Nat.le_trans with (length l). hyp. apply Nat.le_succ_diag_r. Qed.
imports: Coq(PeanoNat) CoLoR(ListUtil ListNodup LogicUtil RelMidex)