proposition: Lemma sorted_dvd0r (s : seq R) : sorted %|%R (0 :: s) -> all (eq_op^~ 0) s.
proof: Proof. move/(order_path_min dvdr_trans)/(all_nthP 0)=> hi. by apply/(all_nthP 0) => i his; rewrite -dvd0r; apply: hi. 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