proposition: Lemma GR_example: GR 10 = 2.
proof: Proof. have Ha n: GRr 1 n = (n <= 3). by rewrite GRr_Sbn !GRr_0n; case:n => [ | [| [ | [ | n]]]]. have ha: GRr 3 2 = 1 by rewrite -(@GRr_big0 1 3 2) // GRr_Sbn ! GRr_0n. rewrite /GR; rewrite -(@GRr_big0 4 10 10) // GRr_Sbn muln1 ha GRr_Sbn muln1. by rewrite (@GRr_notz 2 10) // GRr_Sbn ! Ha. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)