proposition: Lemma order_product_opp_osr g: order_fam g -> order_on (order_product (fam_of_opp g)) (prod_of_substrates g) /\ order_product (fam_of_opp g) = opp_order (order_product g).
proof: Proof. move => ofg. set g' := fam_of_opp g. have ha: allf g sgraph by move => i /ofg []. have hb: domain g = domain g' by rewrite /g' /fam_of_opp; aw. move: (fam_of_opp_sr ha); rewrite -/g' => ff'. have ss': (prod_of_substrates g')= (prod_of_substrates g). by rewrite /prod_of_substrates ff'. have hc: order_fam g' by apply:fam_of_opp_or. move: (order_product_osr hc); rewrite ss' => hd; split => //. move: (order_product_osr hc) => [opg' spg']. move: (order_product_osr ofg) => [opg spg]. move: (opp_osr opg) => [ro _]. apply:order_exten => // x y; split. move /order_product_gleP => [pa pb pc]; apply /opp_gleP. apply/order_product_gleP; split; rewrite -? ss' // => i idg. apply /opp_gleP. rewrite hb in idg; move:(pc _ idg); rewrite LgV//; ue. move /opp_gleP /order_product_gleP => [pa pb pc]. apply/order_product_gleP; split; rewrite ? ss' // => i idg. rewrite - hb in idg; move:(pc _ idg); rewrite LgV// => hh. by apply /opp_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)