proposition: Theorem flatten_valid : forall t:bin, bin_nat t = bin_nat (flatten t).
proof: Proof. intros t; elim t; simpl; auto. intros t1 IHt1 t2 IHt2; rewrite <- flatten_aux_valid; rewrite <- IHt2. trivial. Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure Zdiv