proposition: Lemma min_snum_subproof (xnz ynz : nullity) (xr yr : reality) (x : {compare x0 & xnz & xr}) (y : {compare x0 & ynz & yr}) (rnz := min_nonzero_subdef xnz ynz xr yr) (rrl := min_reality_subdef xnz ynz xr yr) : Signed.spec x0 rnz rrl (Order.min x%:num y%:num).
proof: Proof. rewrite {}/rnz {}/rrl; apply/andP; split. move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y; rewrite /Order.min; do ?[by case: (bottom x)|by case: (bottom y) |by case: ifP; rewrite ?eq0F// => xlty; have := !! lt_trans xlty (lt0 y); rewrite lt_neqAle => /andP[] |by rewrite ifT ?eq0F//; apply: lt_le_trans (ge0 y); exact: lt0 |by have := !! le0 y; rewrite le_eqVlt => /predU1P[->|]; rewrite ?lt0 ?eq0F//; case: ifP => _; rewrite ?eq0F// lt_neqAle => /andP[]]. have /orP[x0ley|] := !! cmp0 y. by rewrite ifT ?eq0F//; apply: lt_le_trans x0ley; exact: lt0. rewrite le_eqVlt => /predU1P[->|]; rewrite ?lt0 ?eq0F//. by case: ifP => _; rewrite ?eq0F// lt_neqAle => /andP[]. move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y; do ?[by case: (bottom x)|by case: (bottom y) |by apply: comparable_minr; exact: cmp0 |by rewrite minEle; case: ifP; rewrite ge0 |by rewrite ?eq0 minEle ?ge0 |by rewrite ?eq0 minElt; case: ifP; rewrite ?eq0// lt0F |by rewrite minEle; case: ifP => [xlty|]; rewrite ?le0//; apply: (le_trans xlty); rewrite le0 |by have /orP[x0ley|] := !! cmp0 y; [rewrite minEle ifT ?le0//; apply: le_trans x0ley; exact: le0 |rewrite minEle; case: ifP => //; exact: le_trans]]. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)