proposition: Lemma IFE_tor : total_order IFS_order.
proof: Proof. move: IFE_osr => [or sr ]; split => //. rewrite sr => x y xE yE. move/Zo_S: (xE) => /setX_P [ra /setX_P [rb rc rd] re]. move/Zo_S: (yE) => /setX_P [ra' /setX_P [rb' rc' rd'] re']. case: (NleT_ell rc rc'). move => eq1; case: (qleT_ell re re'). move => eq2; case: (NleT_ee rd rd') => ll. by left; apply/IFE_gleP; split => //; constructor 3. by right; apply/IFE_gleP; split => //; constructor 3. by left; apply/IFE_gleP; split => //; constructor 2. by right; apply/IFE_gleP; split => //; constructor 2. by left;apply/IFE_gleP; split => //; constructor 1. by right ;apply/IFE_gleP; split => //; constructor 1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)