proposition: Lemma tuto_predU1l : forall x y b, x = y -> (x == y) || b.
proof: Proof. by move=> x y b exy; rewrite exy eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset)