proposition: Lemma maxn_snum_subproof (xnz ynz : nullity) (xr yr : reality) (x : {compare 0 & xnz & xr}) (y : {compare 0 & ynz & yr}) (rnz := max_nonzero_subdef xnz ynz xr yr) (rrl := max_reality_subdef xnz ynz xr yr) : Signed.spec 0 rnz rrl (maxn x%:num y%:num).
proof: Proof. rewrite {}/rnz {}/rrl; apply/andP; split; move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//=; by move=> [[|x]//= _] [[|y]//= _]; rewrite maxnSS. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)