fact: Parameter Z_btree_rect : forall f:Z_btree->Type, f Z_leaf -> (forall (n:Z)(t1:Z_btree), f t1 -> forall t2:Z_btree, f t2 -> f (Z_bnode n t1 t2))-> forall t:Z_btree, f t.
imports: ZArith List Arith Zwf Relations Inverse_Image