proposition: Lemma in_split_r : forall (l:list (A*B))(p:A*B), In p l -> In (snd p) (snd (split l)).
proof: Proof. intro l. induction l as [|[? ?] l IHl]; [easy|]. intros [? ?]. cbn. now intros [[=]|? %IHl]; destruct (split l); [left|right]. Qed.
imports: PeanoNat