proposition: Lemma transpose_nb_occ: forall (l l' : list A), transpose l l' -> forall (a : A), nb_occ a l = nb_occ a l'.
proof: Proof. intros l l' H; elim H; simpl. - intros a b l0 x; case (A_eq_dec x a); case (A_eq_dec x b); simpl; auto. - intros a l0 l'0 H0 H1 x; case (A_eq_dec x a); simpl; auto. Qed.
imports: List Arith