proposition: Theorem remove_neutral1_valid_A: forall (l : list A) (t : bin), bin_A l (remove_neutral1 t) = bin_A l t.
proof: Proof. intros l t; elim t; auto. intros t1; case t1; simpl. - intros t1' t1'' IHt1 t2 IHt2; rewrite IHt2; trivial. - intros n IHt1 t2 IHt2; rewrite IHt2; trivial. - intros IHt1 t2 IHt2; rewrite zero_left; trivial. Qed.
imports: ZArith List Arith Zwf Relations Inverse_Image Transitive_Closure Zdiv