proposition: Lemma set1_order_is2 r r': order r -> order r' -> singletonp (substrate r) -> singletonp (substrate r') -> r \Is r'.
proof: Proof. move=> ox oy ssx ssy. move: (set1_order_is1 ox ssx)=> [u ->]. move: (set1_order_is1 oy ssy)=> [v ->]. apply: set1_order_is. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)