proposition: Lemma norm0_lt : forall a, a != 0 -> norm 0 < norm a.
proof: Proof. move=> a a0; case: (edivP a a)=> q r ha; rewrite a0 /= => hr. apply: leq_trans (hr); rewrite ltnS; apply: contraLR hr. move/eqP: ha; rewrite addrC -(can2_eq (@addrNK _ _) (@addrK _ _)). rewrite -{1}[a]mul1r -mulrBl eq_sym -leqNgt. have [-> | q1] := eqVneq (1 - q) 0; rewrite ?mul0r => /eqP->; rewrite ?leqnn //. by move=> _; rewrite norm_mul. 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