proposition: Lemma fam_of_opp_or g: order_fam g -> order_fam (fam_of_opp g).
proof: Proof. move => h i; rewrite /fam_of_opp Lgd => ig; rewrite LgV//. exact: (proj1 (opp_osr (h i ig))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)