proposition: Lemma GRr_0n n: GRr 0 n = (n<=1).
proof: Proof. move: (@GRr_notz 0 n);rewrite !ltnS; case: n; first by rewrite GRr_b0. by case; [ by rewrite GRr_b1 | move => n]; rewrite !ltnS ltn0; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)