proposition: Lemma orprod_total3P: allf g ne_substrate -> ( (allf g total_order) <-> total_order (order_prod r g)).
proof: Proof. move=> alne; split; first by apply: orprod_total => //. by case: (orprod_total2 alne). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)