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