proposition: Lemma enumerate_no_collisions n : collision (enumerate n) = false.
proof: Proof. induction n. reflexivity. simpl. rewrite IHn. cut (forall a b, a <= b -> appears b (enumerate a) = false). { intros ->; auto. } clear. intros a. induction a; intros b Hb. - reflexivity. - simpl. rewrite IHa. 2:lia. replace (b =? a) with false; auto. symmetry. apply Nat.eqb_neq. lia. Qed.
imports: Arith ZArith List Lia