rename AffineFunction to Affine to be shorter and closer to MathComp
and propagate
fix and reveal [affine ...] notations
scoping was making id point to Coq reals!
we can now use the notation in convex and monae
move affine_function_at to inside Module Affine
it caused useless unfoldings
it now uses the morph notation
it is recovered as the affine_conv lemma which is now
used more efficiently
removed a few occurrences of affine hypotheses in favor of {affine -> }
together with changes above, this improves automatic inference and
therefore shortens proofs
see for example the removal of image_preserves_convex_hull' and
is_convex_set_image' or changes in sections with_affine_projection
and Section S1_proj_Convn_finType
replace affinefunction{id,comp} with more disciplined {idfun,comp}_affine
@t6s