proposition: Lemma combine_app_app : forall A B (l1:list A) (l21 l22: list B), length l21 <= length l1 -> combine l1 (l21 ++ l22) = combine l1 l21 ++ combine (skipn (length l21) l1) (firstn (length l1-length l21) l22).
proof: Proof. induction l1; intros ? ? Hle. inverts Hle. trw_h length0 H0. subst. simpl. auto. simpl. destruct l21; destruct l22; simpl; auto; try omega. - fold (app nil l22). rewrite IHl1. rewrite combine_nil. simpl. assert (length l1 - 0 =length l1) as Hmin by omega. rewrite Hmin. auto. simpl. omega. - rewrite app_nil_r. rewrite firstn_nil. rewrite combine_nil. rewrite app_nil_r. auto. - simpl in Hle. simpl. rewrite IHl1; auto; omega. Qed.
imports: UsefulTypes bin_rels Omega