proposition: Theorem app_nil_r : forall l : natlist, l ++ [] = l.
proof: Proof. MProof. Admitted. Theorem rev_app_distr: forall l1 l2 : natlist, rev (l1 ++ l2) = rev l2 ++ rev l1. MProof. Admitted. Theorem rev_involutive : forall l : natlist, rev (rev l) = l. MProof. Admitted. Theorem app_assoc4 : forall l1 l2 l3 l4 : natlist, l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4. MProof. Admitted. Lemma nonzeros_app : forall l1 l2 : natlist, nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2). MProof. Admitted. Fixpoint beq_natlist (l1 l2 : natlist) : bool . Admitted. Example test_beq_natlist1 : (beq_natlist nil nil = true). Admitted. Example test_beq_natlist2 : beq_natlist [1;2;3] [1;2;3] = true. Admitted. Example test_beq_natlist3 : beq_natlist [1;2;3] [1;2;4] = false. Admitted. Theorem beq_natlist_refl : forall l:natlist, true = beq_natlist l l. MProof. Admitted. Theorem count_member_nonzero : forall (s : bag), leb 1 (count 1 (1 :: s)) = true. MProof. Admitted. Theorem ble_n_Sn : forall n, leb n (S n) = true. MProof. intros n. elim n &> [i:~~| \n' IHn']. - simpl. reflexivity. - simpl. rewrite IHn'. reflexivity. Qed.