proposition: Lemma prod_inj A B : injective (uncurry (@pair A B)).
proof: Proof. by move=> [? ?] [? ?]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)