fact: Definition Ex4_10_conc r n := exists g, [/\ order_fam g, (allf g total_order), cardinal (domain g) = n , (forall i, inc i (domain g) -> substrate (Vg g i) = substrate r) & r = intersectionb g].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)