proposition: Lemma member_app : forall (x : M) (l k : (list M)), (Iff (member x (app k l)) ((member x k) or (member x l))).
proof: Proof. induction k; firstorder. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)