cases H (_); cases (H8 y); apply H9; cases (H8 p);
lapply (H12 H1) as H13; apply (le_le_eq);
[1: apply (le_transitive ???? H4); apply (Le≪ ? H13); assumption;
cases H (_); cases (H8 y); apply H9; cases (H8 p);
lapply (H12 H1) as H13; apply (le_le_eq);
[1: apply (le_transitive ???? H4); apply (Le≪ ? H13); assumption;