- ncases r1; ncases r2; #l2; #u2; #r2; #l1; #u1; #r1
- [ ##1: @1; napplyS (locate_add … r1 …r2);
- ##|##4: @2; napplyS (locate_add … r1 …r2);
- ##| ninversion r2; #q; #q0; #H; #K;
- ndestruct; #U; nrewrite < U in H ⊢ %; #r2';
- ninversion r1;#q; #q0; #H; #K;
- nrewrite < K in H ⊢ %; #H; #J; nrewrite < J in H;
- #r1';
- ##[ @; nlapply (locate_add …r1'…r2'); #H;
-
- .
+ ninversion r1; ninversion r2; #l2'; #u2'; #leq2l; #leq2u; #r2;
+ #l1'; #u1'; #leq1l; #leq1u; #r1
+ [ ##1,4: ##[ @1 ? (l1'+l2') (u1'+u2') | @2 ? (l1'+l2') (u1'+u2') ]
+ ##[ ##1,5: /2/ | napplyS (Qle_plus_compat …leq1u leq2u) |
+ ##4: napplyS (Qle_plus_compat …leq1l leq2l)
+ |##*: /2/ ]
+ ##| ninversion r2; #l2''; #u2''; #leq2l'; #leq2u'; #r2';
+ ninversion r1; #l1''; #u1''; #leq1l'; #leq1u'; #r1';
+ ##[ @1 ? (l1''+l2'') (u1''+u2'');
+ ##[ napply Qle_plus_compat; /3/;
+ ##| ##3: /2/;
+ ##| napplyS (Qle_plus_compat …leq1u' leq2u');
+ .