HB.howto fails to inform the user about smart factories

[CohenCyril]

In the context of mathcomp we use can_type (and others) as a leightweight factory for equality, choice, countability, finiteness by cancellation. HB.howto is not aware of that and fails to inform a user.

Reduced example:

From HB Require Import structures.

HB.mixin Record hasPoint T := { point : T }.
HB.structure Definition Pointed := { T of hasPoint T }.
HB.instance Definition _ := hasPoint.Build unit tt.

(* types which are the image of a pointed type are pointed *)
Definition image_type {T} {iT} (f : T -> iT) := iT.
HB.instance Definition _ (pT : Pointed.type) iT (f : pT -> iT) :=
   hasPoint.Build (image_type f) (f point).

(* HB.howto does not know image_type can be used to make a Pointed.type *)
HB.howto Pointed.type.
HB.instance Definition _ := Pointed.on (image_type (fun _ : unit => true)).

Ideally we would annotate the instance on image_type to flag it as a lightweight factory, for example with an attribute #[light-factory]

[gares]

Also the PcanXXXMixin are not listed but should.

[proux01]

Related to #471

[CohenCyril]

1. light factories coming from aliases can be automatically found through a HB.alias command (HB command for aliases #471)
2. light factories coming from definitions producing factories, should be tagable in some way for HB to know their existence.