fact: Fixpoint choice_type_lt (t1 t2 : choice_type) := match t1, t2 with | chUnit, chUnit => false | chUnit, _ => true | chBool, chUnit => false | chBool, chBool => false | chBool, _ => true | chNat, chUnit => false | chNat, chBool => false | chNat, chNat => false | chNat, _ => true | chProd _ _, chUnit => false | chProd _ _, chBool => false | chProd _ _, chNat => false | chProd u1 u2, chProd w1 w2 => (choice_type_lt u1 w1) || (choice_type_eq u1 w1 && choice_type_lt u2 w2) | chProd _ _, _ => true | chMap _ _, chUnit => false | chMap _ _, chBool => false | chMap _ _, chNat => false | chMap _ _, chProd _ _ => false | chMap u1 u2, chMap w1 w2 => (choice_type_lt u1 w1) || (choice_type_eq u1 w1 && choice_type_lt u2 w2) | chMap _ _, _ => true | chOption _, chUnit => false | chOption _, chBool => false | chOption _, chNat => false | chOption _, chProd _ _ => false | chOption _, chMap _ _ => false | chOption u, chOption w => choice_type_lt u w | chOption _, _ => true | chFin n, chUnit => false | chFin n, chBool => false | chFin n, chNat => false | chFin n, chProd _ _ => false | chFin n, chMap _ _ => false | chFin n, chOption _ => false | chFin n, chFin n' => n < n' end.
imports: Coq(Utf8 Lia) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples GenericRulesSimple) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr realsum seq all_algebra fintype) Crypt(Prelude Axioms) extructures(ord fset fmap) Mon(SPropBase) Equations(Equations)