proposition: Lemma indecomp_diff2 c: \0o <o c -> (forall a, a <o c -> c -o a = c) ->indecomposable c.
proof: Proof. move => oc cp. apply/(indecompP oc) => a lac. by rewrite -{1} (cp _ lac) -(proj2 (odiff_pr (proj1 lac))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)