proposition: Lemma inj_pair A B (a1 a2 : A) (b1 b2 : B) : (a1, b1) = (a2, b2) -> (a1 = a2) * (b1 = b2).
proof: Proof. by case. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms)