proposition: Lemma normCBeq x y : `|x - y| = `|x| - `|y| -> {t | `|t| == 1 & (x, y) = (`|x| * t, `|y| * t)}.
proof: Proof. set z := x - y; rewrite -(subrK y x) -/z => /(canLR (subrK _))/esym-Dx. have [t t_1 [Dz Dy]] := normCDeq Dx. by exists t; rewrite // Dx mulrDl -Dz -Dy. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)