fact: Fixpoint flatten_aux (t fin:bin){struct t} : bin := match t with | node t1 t2 => flatten_aux t1 (flatten_aux t2 fin) | x => node x fin end.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure Zdiv