proposition: Lemma sorted_nth0 (s : seq R) : sorted %|%R s -> forall i, s`_0 %| s`_i.
proof: Proof. case: s=> [_|a s hi] [|i] /=; do? by rewrite dvdrr. have [his|hsi] := ltnP i (size s); last by rewrite nth_default // dvdr0. by move/(order_path_min dvdr_trans)/(all_nthP 0): 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