proposition: Lemma max_snum_subproof (xnz ynz : nullity) (xr yr : reality) (x : {compare x0 & xnz & xr}) (y : {compare x0 & ynz & yr}) (rnz := max_nonzero_subdef xnz ynz xr yr) (rrl := max_reality_subdef xnz ynz xr yr) : Signed.spec x0 rnz rrl (Order.max x%:num y%:num).
proof: Proof. rewrite {}/rnz {}/rrl; apply/andP; split. move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y; rewrite maxElt; do ?[by case: (bottom x)|by case: (bottom y) |by case: ifP => [xlty|]; rewrite ?eq0F//; do [suff : (x0 < y%:num)%O by rewrite lt_def => /andP[]]; apply: le_lt_trans xlty; exact: ge0 |by rewrite ifT ?eq0F//; apply: le_lt_trans (gt0 y); exact: le0 |by have := !! ge0 x; rewrite le_eqVlt => /predU1P[<-|]; rewrite ?gt0 ?eq0F//; case: ifP => _; rewrite ?eq0F// lt_def => /andP[]]. have /orP[|xlex0] := !! cmp0 x. rewrite le_eqVlt => /predU1P[<-|]; rewrite ?gt0 ?eq0F//. by case: ifP => _; rewrite ?eq0F// lt_def => /andP[]. by rewrite ifT ?eq0F//; apply: (le_lt_trans xlex0); exact: gt0. move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y; do ?[by case: (bottom x)|by case: (bottom y) |by apply: comparable_maxr; exact: cmp0 |by rewrite ?eq0 maxEle ?le0 |by rewrite ?eq0 maxElt ifF// le_gtF// le0 |by rewrite maxEle; case: ifP; rewrite ?ge0//; exact/le_trans/ge0 |by rewrite maxElt; case: ifP => [xlty|]; rewrite ?le0// |by have /orP[|xlex0] := !! cmp0 x; [rewrite maxEle; case: ifP => // /[swap]; exact: le_trans |rewrite maxEle ifT ?ge0//; apply: (le_trans xlex0); exact: ge0]]. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)