Simplify Cauchy_prod.cauchy_finite proof
Simplify Cauchy_prod.cauchy_finite proof

We use strict focusing, trying to finish shorter subgoals first

(ie typically we have
~~~
replace foo with bar.
lots of stuff.
a few tactics proving foo = bar.
~~~
which becomes
~~~
replace foo with bar.
2:{ a few tactics proving foo = bar. }
lots of stuff.
~~~
)

We also remove hundreds of lines by using auto with zarith.

coq/coq,Zimmi48/coq,ejgallego/coq,Zimmi48/coq,SkySkimmer/coq,Zimmi48/coq,Zimmi48/coq,coq/coq,coq/coq,SkySkimmer/coq,coq/coq,ejgallego/coq,SkySkimmer/coq,ejgallego/coq,SkySkimmer/coq,ejgallego/coq