proposition: Theorem eqbP_practice : forall n l, count n l = 0 -> ~(In n l).
proof: Proof. intros n l Hcount. induction l as [| m l' IHl']. Admitted. Inductive nostutter {X:Type} : list X -> Prop := . Example test_nostutter_1: nostutter [3;1;4;1;5;6]. Admitted. Example test_nostutter_2: nostutter (@nil nat). Admitted. Example test_nostutter_3: nostutter [5]. Admitted. Example test_nostutter_4: not (nostutter [3;1;1;4]). Admitted. Definition manual_grade_for_nostutter : option (nat*string) := None. Definition manual_grade_for_filter_challenge : option (nat*string) := None. Definition manual_grade_for_pal_pal_app_rev_pal_rev : option (nat*string) := None. Definition manual_grade_for_NoDup_disjoint_etc : option (nat*string) := None. Lemma in_split : forall (X:Type) (x:X) (l:list X), In x l -> exists l1 l2, l = l1 ++ x :: l2. Proof. Admitted. Inductive repeats {X:Type} : list X -> Prop := . Definition manual_grade_for_check_repeats : option (nat*string) := None. Theorem pigeonhole_principle: excluded_middle -> forall (X:Type) (l1 l2:list X), (forall x, In x l1 -> In x l2) -> length l2 < length l1 -> repeats l1. Proof. intros EM X l1. induction l1 as [|x l1' IHl1']. Admitted. Require Import Coq.Strings.Ascii. Definition string := list ascii. Lemma provable_equiv_true : forall (P : Prop), P -> (P <-> True). Proof. intros. split. - intros. constructor. - intros _. apply H. Qed.
imports: Coq(Lia)