+*)
+
+nlemma help_auto1: ∀q:Q. false * q = 0. #q; nnormalize; //. nqed.
+
+(*
+nlet corec locate_add (l,u:?) (r1,r2: locate l u) (c1,c2:bool) :
+ locate (l + l + c1 * phi + c2 * phi * phi) (u + u + c1 * phi + c2 * phi * phi) ≝ ?.
+ napply (locate_inv_ind' … r1); napply (locate_inv_ind' … r2);
+ #r2'; #r1'; ncases c1; ncases c2
+ [ ##4: nnormalize; @1;
+ nlapply (locate_add … r1' r2' false false); nnormalize;
+ nrewrite > (Qmult_zero …); nrewrite > (Qmult_zero …); #K; nauto demod;
+ #K;
+ nnormalize in K; nrewrite > (Qmult_zero …) in K; nnormalize; #K;
+ napplyS K;
+
+
+
+
+ [ ##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');