proposition: Lemma check_prime n : (do_check1 n) && (do_check2 n) -> prime n.
proof: Proof. Abort. Print Bool.reflect. Lemma trueP : reflect True true. Proof. by constructor. Qed.
imports: mathcomp(ssreflect ssrnat prime ssrbool eqtype)