+try (apply ap_symmetric; assumption); intros 4 (x y z H); change with (0 < (δ y z));
+[ change in H with (0 < δ (x ∨ y) (x ∨ z));
+ apply (lt_le_transitive ???? H);
+ apply (le0plus_le ???? (mpositive ? pml ??) (prop5 ? pml pml x y z));
+| change in H with (0 < δ (x ∧ y) (x ∧ z));
+ apply (lt_le_transitive ???? H);
+ apply (le0plus_le ???? (mpositive ? pml (x∨y) (x∨z)));
+ apply (le_rewl ??? ? (plus_comm ???));
+ apply (prop5 ? pml pml);]