proposition: Lemma eq_invF f g injf injg : f =1 g -> @invF T f injf =1 @invF T g injg.
proof: Proof. by move=> eq_fg x; apply: (canLR (invF_f injf)); rewrite eq_fg f_invF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)