proposition: Lemma ltn_norm : forall a b, b != 0 -> a %<| b -> norm a < norm b.
proof: Proof. move=> a b b0; case/andP=> ab. case: (edivP a b)=> q r; rewrite b0 /= => ha nrb; rewrite {1}ha. have [-> | r0] := eqVneq r 0; first by rewrite addr0 dvdr_mull. rewrite dvdr_addr ?dvdr_mull // (leq_trans _ nrb) // ltnS leq_norm ?r0 //. by move: (dvdrr a); rewrite {2}ha dvdr_addr ?dvdr_mull. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool Arith.Wf_nat) mathcomp(eqtype ssrnat div seq path) mathcomp(ssralg fintype perm tuple choice generic_quotient) mathcomp(matrix bigop zmodp mxalgebra poly) stronglydiscrete