proposition: Theorem mul_reg_r p q r : p * r = q * r -> p = q.
proof: Proof. revert q r. induction p as [p IHp| p IHp| ]; intros [q|q| ] r H; reflexivity || apply f_equal || exfalso. - apply IHp with (r~0). simpl in *. rewrite 2 mul_xO_r. apply add_reg_l with (1:=H). - contradict H. apply mul_xI_mul_xO_discr. - contradict H. simpl. rewrite add_comm. apply add_no_neutral. - symmetry in H. contradict H. apply mul_xI_mul_xO_discr. - apply IHp with (r~0). simpl. now rewrite 2 mul_xO_r. - contradict H. apply mul_xO_discr. - symmetry in H. contradict H. simpl. rewrite add_comm. apply add_no_neutral. - symmetry in H. contradict H. apply mul_xO_discr. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef