From mathcomp Require Import all_ssreflect. Lemma test n : 0 <= n. Proof. by []. Qed.
Please wait until loaded (something like 10 seconds) then press ALT-N and ALT-P to process the document forward and backward. Note: the first line takes a few seconds to run.
(* The Coq source continues down here... *)
save script
load script