fact: Fixpoint bin_A (l : list A) (t : bin) {struct t} : A := match t with node t1 t2 => f (bin_A l t1) (bin_A l t2) | leaf n => nth n l zero_A | neutral => zero_A end.
imports: ZArith List Arith Zwf Relations Inverse_Image Transitive_Closure Zdiv