proposition: Lemma OT_1_least_nz x: order_type x -> x <> emptyset -> \1t <=t x.
proof: Proof. move:OT_1_order_type => ha hb hc; apply/OTorder_le_altP; split => //. move:(OT_prop2 ha) (OT_prop2 hb) => oa ob. set E := substrate x. case: (emptyset_dichot E);[ by move/empty_substrate_zero | move =>[a aE]]. move: singleton_OT_pr =>[b bp]. move: (set1_wor b); rewrite - bp; move =>[wo1 sr1]. pose f := Lf (fun z => a )(singleton b) E. have ax: lf_axiom (fun _ => a) (singleton b) E by move => t. exists f. split => //; first by rewrite/f;saw; [ by apply:lf_function | done]. hnf;rewrite /f ; aw => u v ud vd; rewrite ! LfV//; split => _; first by order_tac. by rewrite (set1_eq ud) (set1_eq vd) bp; apply: set1_1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)