proposition: Theorem reflection_test' : forall x y z t u:nat, x+(y+z+(t+u))=x+y+(z+(t+u)).
proof: Proof. intros. change (bin_nat (node (leaf x) (node (node (leaf y) (leaf z)) (node (leaf t)(leaf u)))) = bin_nat (node (node (leaf x)(leaf y)) (node (leaf z) (node (leaf t)(leaf u))))). apply flatten_valid_2; auto. Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure Zdiv