proposition: Lemma lt_total : forall f g, beq_symb f g = false -> blt f g = false -> blt g f = true.
proof: Proof. intros f g. unfold blt. rewrite bgt_nat_ok, bgt_nat_ko, (beq_ko (@beq_symb_ok Sig)). intros. destruct (eq_nat_dec (weight f) (weight g)). ded (weight_inj e). subst g. cong. lia. Qed.
imports: CoLoR(EqUtil ListUtil LogicUtil) Coq(DecidableType) CoLoR(NatUtil BoolUtil) Coq(OrderedType)