rm tests in`itv.v` (now `interval_inference.v`)

[affeldt-aist]

analysis/theories/itv.v

Lines 845 to 891 in 36680bc

	Section Test1.
	Variable R : numDomainType.
	Variable x : {i01 R}.
	Goal 0%:i01 = 1%:i01 :> {i01 R}.
	Abort.
	Goal (- x%:inum)%:itv = (- x%:inum)%:itv :> {itv R & `[-1, 0]}.
	Abort.
	Goal (1 - x%:inum)%:i01 = x.
	Abort.
	End Test1.
	Section Test2.
	Variable R : realDomainType.
	Variable x y : {i01 R}.
	Goal (x%:inum * y%:inum)%:i01 = x%:inum%:i01.
	Abort.
	End Test2.
	Module Test3.
	Section Test3.
	Variable R : realDomainType.
	Definition s_of_pq (p q : {i01 R}) : {i01 R} :=
	(1 - ((1 - p%:inum)%:i01%:inum * (1 - q%:inum)%:i01%:inum))%:i01.
	Lemma s_of_p0 (p : {i01 R}) : s_of_pq p 0%:i01 = p.
	Proof.
	apply/val_inj => /=.
	by rewrite subr0 mulr1 opprB addrCA subrr addr0.
	Qed.
	Canonical onem_itv01 (p : {i01 R}) : {i01 R} :=
	@Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum].
	Definition s_of_pq' (p q : {i01 R}) : {i01 R} :=
	(`1- (`1-(p%:inum) * `1-(q%:inum)))%:i01.
	End Test3.
	End Test3.

or at the very least provide a better (informative?) set of tests