proposition: Lemma Exercise4_7d: inc (the_least r) (irreds r).
proof: Proof. move: Exercise4_7b Exercise4_7c => or el. move: (the_least_pr or el) => [p1 p2]. apply: (Zo_i p1); case: (Exercise4_7a p1) => //- [a [_ [al _ _]]]. have asr: inc a (substrate r) by order_tac. move: (p2 _ asr) => p3; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)