proposition: Lemma IFE_osr : order_on IFS_order IFSE.
proof: Proof. have Ha a: inc a IFSE -> IFS_order_rel1 a a by move => _; left. move: (graph_on_sr Ha); rewrite -/IFS_order => se. split => //. apply:order_from_rel; split. - move => b a c qa qb. case: (qa); [ by move -> | move => qa' ]. case: qb; [by move <- | case => qb; case: qa' => qc]. - right; constructor 1; apply: (clt_ltT qc qb). - by right; constructor 1; rewrite (proj1 qc). - by right; constructor 1; rewrite (proj31 qc). - by right; constructor 1; rewrite - (proj1 qb). - right; constructor 2; move: qc qb => [-> ra] [-> rb]; split => //. by apply: (qlt_ltT ra rb). - by right; constructor 2; move: qc qb => [-> -> rb] [-> rc]. - by right; constructor 1; rewrite - (proj31 qb). - by right; constructor 2; move: qc qb => [-> ra] [-> <- rc]. - right; constructor 3; move: qc qb => [-> -> ra] [-> <- rc]. by split => //; apply: (clt_ltT ra rc). - move => a b. case => // qa; case => // qb. case: qa; case: qb => qa qb. - by move:(cleNgt (proj1 qa) qb). - case: (proj2 qb); exact: (esym (proj1 qa)). - case: (proj2 qb); exact: (esym (proj31 qa)). - case: (proj2 qa); exact: (esym (proj1 qb)). - case:(qleNgt (proj1 (proj2 qa)) (proj2 qb)). - case: (proj2 (proj2 qb)); exact: (esym (proj32 qa)). - case: (proj2 qa); exact: (esym (proj31 qb)). - case: (proj2 (proj2 qa)); exact: (esym (proj32 qb)). - case: (cleNgt (proj1 (proj33 qa)) (proj33 qb)). by move => a b _; split; left. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)