theorem immoral_non_rich_twin_makes_rich_twin_immoral
theorem immoral_non_rich_twin_makes_rich_twin_immoral
(coherent : MoralComparisonIsCoherent)
(immoral_below : ImmoralBelowNonImmoral)
(rich_less_moral : AllElseEqualTheRichPersonIsLessMoral)
: ∀ (s : TwoPeopleDifferingInWealth), s.p2.val is-immoral → s.p1.val is-immoral