proposition: Lemma position_ko : forall x l, position x l = None <-> ~In x l.
proof: Proof. unfold position. cut (forall x l i, position_aux i x l = None <-> ~In x l). auto. induction l; simpl; intros. intuition. case_beq x a. intuition; discr. rewrite (beq_ko beq_ok) in H. ded (IHl (S i)). intuition. Qed.
imports: Coq(Arith Lia) CoLoR(ListUtil BoolUtil EqUtil LogicUtil)