proposition: Lemma ord_prime_prop1 a: ord_sprime a -> ord_prime a.
proof: Proof. move => [oa ag1 H]; split => // b c ob oc eq1; rewrite eq1. case:(H b c ob oc eq1) => ->. by right;rewrite (oprod1l oc). by left;rewrite (oprod1r ob). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)