proposition: Lemma check_prime n : (do_check1 n) && (do_check2 n) -> prime n.
proof: Proof. Abort. Module Inner. Inductive reflect (P : Prop) : bool -> Set := | ReflectT of P : reflect P true | ReflectF of ~ P : reflect P false. End Inner. Lemma trueP : reflect True true. Proof. by constructor. Qed.
imports: mathcomp(ssreflect ssrfun eqtype ssrnat ssrbool prime eqtype)