proposition: Theorem sort_eq : forall (l:list A)(def:A)(t:bin), bin_A' l def (sort_bin t) = bin_A' l def t.
proof: Proof. intros l def t; elim t. intros t1 IHt1; case t1. auto. intros n t2 IHt2; simpl; rewrite insert_is_f. rewrite IHt2; auto. auto. Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure Zdiv