proposition: Theorem flatten_valid_A: forall (l : list A) (t : bin), bin_A l t = bin_A l (flatten t).
proof: Proof. intros l t; elim t; simpl; trivial. intros t1 IHt1 t2 IHt2; rewrite <- flatten_aux_valid_A; now rewrite <- IHt2. Qed.
imports: ZArith List Arith Zwf Relations Inverse_Image Transitive_Closure Zdiv