Remove code PRed to MathComp

[affeldt-aist]

analysis/theories/normedtype.v

Lines 3345 to 3361 in 6d6fb39

	Section TODO_add_to_ssrnum.
	Lemma maxr_real (K : realDomainType) (x y : K) :
	x \is Num.real -> y \is Num.real -> maxr x y \is Num.real.
	Proof.
	by rewrite !realE => /orP[|] x0 /orP[|] y0; rewrite le_maxr le_maxl x0 y0 !(orbT,orTb).
	Qed.
	Lemma bigmaxr_real (K : realDomainType) (R : choiceType) (x : K) (D : seq R) (f : R -> K):
	x \is Num.real ->
	(forall x, x \in D -> f x \is Num.real) ->
	\big[maxr/x]_(n <- D) f n \is Num.real.
	Proof.
	move=> ?; elim/big_ind : _ => // *; by [rewrite maxr_real | rewrite num_real].
	Qed.
	End TODO_add_to_ssrnum.

Remove when PR math-comp/math-comp#593 is merged with MathComp's master and released.