proposition: Theorem flatten_valid_2 : forall t t':bin, bin_nat (flatten t) = bin_nat (flatten t')-> bin_nat t = bin_nat t'.
proof: Proof. intros; rewrite (flatten_valid t); rewrite (flatten_valid t'); auto. Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure Zdiv