fact: Definition min (a b : rZ) : rZ := match rZltDec a b with | left _ => a | right _ => b end.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)