Library probsa.util.tr_eq

From mathcomp Require Export ssreflect eqtype.

Lemma eq_tr4 : ∀ {T : eqType} (x y xo yo : T), xo = yo → x = xo → y = yo → x = y.
Proof. by intros; subst. Qed.

Lemma eq_tr3 : ∀ {T : eqType} (x y t : T), x = t → t = y → x = y.
Proof. by intros; subst. Qed.