proposition: Lemma mul_compare_mono_l p q r : (p*q ?= p*r) = (q ?= r).
proof: Proof. revert q r. induction p as [p IHp|p IHp|]; simpl; trivial. intros q r. specialize (IHp q r). destruct (compare_spec q r). - subst. apply compare_refl. - now apply add_lt_mono. - now apply lt_gt, add_lt_mono, gt_lt. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef