`prob` may have two eqType structures, leading to failures in rewriting / applying lemmas.

[t6s]

I experienced this issue when trying to use prob_lt0. The lemma takes as its argument _ : p != 0 and it did not match my goal because of a mismatch between two eqType structures.

One solution would be to change the interface of prob to

Module Prob.
Record t := mk_ {
  p :> R ;
  Op1 : (0 <b= p <b= 1)%R }.
Definition O1 (p : t) : 0 <= p <= 1 :=
  match andP (Op1 p) with conj Op p1 => conj (leRP _ _ Op) (leRP _ _ p1) end.
Arguments O1 : simpl never.
Definition mk (q : R) (Oq1 : 0 <= q <= 1) : t.
Proof.
refine (@mk_ q (match Oq1 with conj Oq q1 => _ end)).
by move/leRP: Oq ->; move/leRP: q1 ->.
Defined.
Module Exports.
Notation prob := t.
Notation "q %:pr" := (@mk q (@O1 _)).
Canonical prob_subType := Eval hnf in [subType for p].
Definition prob_eqMixin := [eqMixin of prob by <:].
Canonical prob_eqType := Eval hnf in EqType _ prob_eqMixin.
End Exports.
End Prob.
Export Prob.Exports.
Coercion Prob.p : prob >-> R.

This seems to almost work, but failing at inferring the canonical structure for onem.