proposition: Lemma order_indep (p: property) (r:= fun x y => p x): order_r r <-> forall x, ~(p x).
proof: Proof. split. move =>[ha hb hc] x0 px0. have py:forall y, (p y) by move => y;exact:(proj2 (hc x0 y px0)). have qy: forall y, x0 = y by move => y; exact:(hb _ _ px0 (py y)). by case:(C0_ne_C1); rewrite -(qy C0) -(qy C1). move => pf; split. - by move => a b c /pf. - by move => a b /pf. - by move => a b /pf. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)