ErVinuelas

Results 1 issues of ErVinuelas

I mostly added comments, but also a new definition for a recurrent pattern and a Ltac tactic associated with it. The `lagrange_poly_part_0` had an extra hypothesis that was not used...