proposition: Lemma false_in_combine_repeat : forall A B (al : list A) (t : B) n, n > 0 -> forall a, LIn a al -> LIn (a,t) (combine al (repeat n t)).
proof: Proof. Abort. Lemma in_combine_repeat : forall A B (al : list A) (t : B) n, length al <= n -> forall a, LIn a al -> LIn (a,t) (combine al (repeat n t)). Proof. induction al; simpl; sp; subst; destruct n; try omega; allapply S_le_inj; simpl; sp. Qed.
imports: UsefulTypes bin_rels Omega