proposition: Lemma leA_comp: forall a, comp_eqA (leA a).
proof: Proof. intros a b c bc ab ca. apply ab. eapply gtA_morph. refl. apply bc. hyp. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)