proposition: Theorem remove_does_not_increase_count: forall (s : bag), (count 0 (remove_one 0 s)) <=? (count 0 s) = true.
proof: Proof. Admitted. Theorem involution_injective : forall (f : nat -> nat), (forall n : nat, n = f (f n)) -> (forall n1 n2 : nat, f n1 = f n2 -> n1 = n2). Proof. Admitted. Theorem rev_injective : forall (l1 l2 : natlist), rev l1 = rev l2 -> l1 = l2. Proof. Admitted. Fixpoint nth_bad (l:natlist) (n:nat) : nat := match l with | nil => 42 | a :: l' => match n with | 0 => a | S n' => nth_bad l' n' end end. Inductive natoption : Type := | Some (n : nat) | None. Fixpoint nth_error (l:natlist) (n:nat) : natoption := match l with | nil => None | a :: l' => match n with | O => Some a | S n' => nth_error l' n' end end. Example test_nth_error1 : nth_error [4;5;6;7] 0 = Some 4. Proof. reflexivity. Qed.