proposition: Theorem app_nil_r : forall l : natlist, l ++ [] = l.
proof: Proof. Admitted. Theorem rev_app_distr: forall l1 l2 : natlist, rev (l1 ++ l2) = rev l2 ++ rev l1. Proof. Admitted. Theorem rev_involutive : forall l : natlist, rev (rev l) = l. Proof. Admitted. Theorem app_assoc4 : forall l1 l2 l3 l4 : natlist, l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4. Proof. Admitted. Lemma nonzeros_app : forall l1 l2 : natlist, nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2). Proof. Admitted. Fixpoint eqblist (l1 l2 : natlist) : bool . Admitted. Example test_eqblist1 : (eqblist nil nil = true). Admitted. Example test_eqblist2 : eqblist [1;2;3] [1;2;3] = true. Admitted. Example test_eqblist3 : eqblist [1;2;3] [1;2;4] = false. Admitted. Theorem eqblist_refl : forall l:natlist, true = eqblist l l. Proof. Admitted. Theorem count_member_nonzero : forall (s : bag), 1 <=? (count 1 (1 :: s)) = true. Proof. Admitted. Theorem leb_n_Sn : forall n, n <=? (S n) = true. Proof. intros n. induction n as [| n' IHn']. - simpl. reflexivity. - simpl. rewrite IHn'. reflexivity. Qed.