proposition: Lemma or_dec P Q : decidable P -> decidable Q -> P \/ Q -> {P} + {Q}.
proof: Proof. case; first by move=> *; left. move=> nP [|nQ]; first by move=> *; right. move=> K; exfalso; by destruct K. Qed.
imports: ZArith NArith FMaps FMapAVL mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice finfun tuple fintype ssralg bigop) CoqEAL(hrel) CoqEAL(refinements) CoqEAL(param binord binnat) CoqEAL(seqmx ) CoqEAL(ssrcomplements) mathcomp.multinomials(mpoly freeg)