proposition: Theorem ptree_meld_correct : forall p1 p2, permut (ptree_to_list (ptree_meld p1 p2)) (ptree_to_list p1 ++ ptree_to_list p2).
proof: Proof. intros [v1 l1] [v2 l2]. unfold ptree_meld. case le ; simpl. - apply permut_cons. apply (permut_app (v2 :: flat_map _ _)). - apply permut_insert with (p := v1 :: flat_map _ _). Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)