proposition: Theorem prod2list_le_r : forall a b c d l1 l2 l3 l4 l5 l6, length l1 = length l4 -> length l2 = length l5 -> length l3 = length l6 -> sum_leaves f d <= sum_leaves f c -> b <= a -> prod2list (l1 ++ a :: l2 ++ b :: l3) (l4 ++ d :: l5 ++ c :: l6) <= prod2list (l1 ++ a :: l2 ++ b :: l3) (l4 ++ c :: l5 ++ d :: l6).
proof: Proof. intros a b c d l1 l2 l3 l4 l5 l6 H H0 H1 H2 H3; change (prod2list (l1 ++ (a :: []) ++ l2 ++ (b :: []) ++ l3) (l4 ++ (d :: []) ++ l5 ++ (c :: []) ++ l6) <= prod2list (l1 ++ (a :: []) ++ l2 ++ (b :: []) ++ l3) (l4 ++ (c :: []) ++ l5 ++ (d :: []) ++ l6)) in |- *. repeat rewrite prod2list_app; auto. apply Nat.add_le_mono; auto with arith. repeat rewrite Nat.add_assoc; apply Nat.add_le_mono; auto. repeat rewrite (fun x y z => Nat.add_comm (prod2list (x :: y) z)). repeat rewrite <- Nat.add_assoc; apply Nat.add_le_mono; auto. unfold prod2list in |- *; simpl in |- *. rewrite <- Nat.sub_add with (1 := H3); auto. rewrite <- Nat.sub_add with (1 := H2); auto. replace ((a - b + b) * (sum_leaves f c - sum_leaves f d + sum_leaves f d) + weight_tree f c + (b * sum_leaves f d + weight_tree f d)) with ((b + (a - b)) * sum_leaves f d + weight_tree f d + ((b + (a - b)) * (sum_leaves f c - sum_leaves f d) + b * sum_leaves f d + weight_tree f c)); [ idtac | ring ]. ring_simplify; auto with arith. Qed.
imports: Coq(ArithRing Sorting.Permutation)