proposition: Lemma qlm : (exists !x, exists !y, Q x y).
proof: Proof. exists true; split; first by exists true; split=> //; case. case=>//; rewrite /Q; case; case=>/=; case=>_ G. - by move:(G false (eqxx false)). by move:(G true (eqxx true)). Qed.
imports: mathcomp(ssreflect ssrnat prime ssrbool eqtype)