proposition: Theorem le_sum_correct2 : forall a b1 : btree A, le_sum a b1 = false -> sum_order b1 a.
proof: Proof. intros a b1 Hsum; apply Nat.leb_gt in Hsum. unfold sum_order; auto with arith. Qed.
imports: Coq(ArithRing Sorting.Permutation)