proposition: Theorem insert_is_f : forall (l:list A)(def:A)(n:nat)(t:bin), bin_A' l def (insert_bin n t) = f (nth n l def) (bin_A' l def t).
proof: Proof. intros l def n t; elim t. intros t1; case t1. intros t1' t1'' IHt1 t2 IHt2. simpl. auto. intros n0 IHt1 t2 IHt2. simpl. case (nat_le_bool n n0). simpl. auto. simpl. rewrite IHt2. repeat rewrite assoc; rewrite (comm (nth n l def)); auto. simpl. intros n0. case (nat_le_bool n n0); auto; try rewrite comm; auto. Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure Zdiv