proposition: Lemma gtA_eqA_compat' : forall a b, eqA a b -> forall c d, eqA c d -> gtA a c -> gtA b d.
proof: Proof. apply gtA_eqA_compat. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)